Search for: All records

Monolithic control plane verification cannot scale to hyperscale network architectures with tens of thousands of nodes, heterogeneous network policies and thousands of network changes a day. Instead, modular verification offers improved scalability, reasoning over diverse behaviors, and robustness following policy updates. We introduce Timepiece, a new modular control plane verification system. While one class of verifiers, starting with Minesweeper, were based on analysis of stable paths, we show that such models, when deployed naïvely for modular verification, are unsound. To rectify the situation, we adopt a routing model based around a logical notion of time and develop a sound, expressive, and scalable verification engine. Our system requires that a user specifies interfaces between module components. We develop methods for defining these interfaces using predicates inspired by temporal logic, and show how to use those interfaces to verify a range of network-wide properties such as reachability or access control. Verifying a prefix-filtering policy using a non-modular verification engine times out on an 80-node fattree network after 2 hours. However, Timepiece verifies a 2,000-node fattree in 2.37 minutes on a 96-core virtual machine. Modular verification of individual routers is embarrassingly parallel and completes in seconds, which allows verification to scale beyond non-modular engines, while still allowing the full power of SMT-based symbolic reasoning. 

Abstract Magnetic and electronic properties of quantum materials heavily rely on the crystal structure even in the same chemical compositions. In this study, it is demonstrated that a layered tetragonal EuCd 2 Sb 2 structure can be obtained by treating bulk trigonal EuCd 2 Sb 2 under high pressure (6 GPa) and high temperature (600 °C). Magnetization measurements of the newly formed layered tetragonal EuCd 2 Sb 2 confirm an antiferromagnetic ordering with Neel temperature ( T N ) around 16 K, which is significantly higher than that ( T N ≈ 7 K) of trigonal EuCd 2 Sb 2 , consistent with heat capacity measurements. Moreover, bad metal behavior is observed in the temperature dependence of the electrical resistivity and the resistivity shows a dramatic increase around the Neel temperature. Electronic structure calculations with local density approximation dynamic mean–field theory (LDA+DMFT) show that this material is strongly correlated with well‐formed large magnetic moments, due to Hund's coupling, which is known to dramatically suppress the Kondo scale. 

The development of programmable switches such as the Intel Tofino has allowed network designers to implement a wide range of new in-network applications and network control logic. However, current switch programming languages, like P4, operate at a very low level of abstraction. This paper introduces SwitchLog, a new experimental logic programming language designed to lift the level of abstraction at which network programmers operate, while remaining amenable to efficient implementation on programmable switches. SwitchLog is inspired by previous distributed logic programming languages such as NDLog, in which programmers declare a series of facts, each located at a particular switch in the network. Logic programming rules that operate on facts at different locations implicitly generate network communication, and are updated incrementally, as packets pass through a switch. In order to ensure these updates can be implemented efficiently on switch hardware, SwitchLog imposes several restrictions on the way programmers can craft their rules. We demonstrate that SwitchLog can be used to express a variety of networking applications in a mere handful of lines of code. 

The P4 language and programmable switch hardware, like the Intel Tofino, have made it possible for network engineers to write new programs that customize operation of computer networks, thereby improving performance, fault-tolerance, energy use, and security. Unfortunately, possible does not mean easy —there are many implicit constraints that programmers must obey if they wish their programs to compile to specialized networking hardware. In particular, all computations on the same switch must access data structures in a consistent order, or it will not be possible to lay that data out along the switch’s packet-processing pipeline. In this paper, we define Lucid 2.0, a new language and type system that guarantees programs access data in a consistent order and hence are pipeline-safe . Lucid 2.0 builds on top of the original Lucid language, which is also pipeline-safe, but lacks the features needed for modular construction of data structure libraries. Hence, Lucid 2.0 adds (1) polymorphism and ordering constraints for code reuse; (2) abstract, hierarchical pipeline locations and data types to support information hiding; (3) compile-time constructors, vectors and loops to allow for construction of flexible data structures; and (4) type inference to lessen the burden of program annotations. We develop the meta-theory of Lucid 2.0, prove soundness, and show how to encode constraint checking as an SMT problem. We demonstrate the utility of Lucid 2.0 by developing a suite of useful networking libraries and applications that exploit our new language features, including Bloom filters, sketches, cuckoo hash tables, distributed firewalls, DNS reflection defenses, network address translators (NATs) and a probabilistic traffic monitoring service.